Nuprl Lemma : not-not-assert
11,40
postcript
pdf
b
:
. (
(
b
))
(
b
)
latex
ProofTree
Definitions
P
Q
,
P
&
Q
,
P
Q
,
Void
,
,
,
Type
,
if
b
then
t
else
f
fi
,
True
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
x
:
A
B
(
x
)
,
P
Q
,
False
,
A
,
b
,
x
:
A
.
B
(
x
)
,
t
T
,
Dec(
P
)
,
P
Q
,
left
+
right
Lemmas
decidable
assert
,
assert
wf
,
not
wf
,
bool
wf
origin
b:
. (
(
b)) 
(b)
b:. ((b)) (b)
Q Q
B(x) QAbx:A. B(x)
T
Q